T:Type, l:(T List), a,x:T.
l_member!(x; cons(a; l); T)  (((x = a)  ((x  l)))  (l_member!(x; l; T)  ((x = a)))) 

latex

Definitions	False, A  B, prop{i:l}, t  T, P  Q, P  Q, A c B, x:A. B(x), A, P  Q, P  Q, l_member!(x; l; T), P  Q, x:A. B(x), , ff, tt, i <z j, b, i z j, if b then t else f fi , Y, nth_tl(n;as), hd(l), l[i], ||as||, True, T, guard(T), sq_type(T), (x  l), decidable(P), nequal(T; a; b)
Lemmas	l member wf, not wf, nat wf, select wf, length wf1, neg assert of eq int, nat sq, le wf, assert of eq int, eq int wf, decidable assert, select cons tl, squash wf, length cons, non neg length, decidable int equal, member wf, true wf, select cons hd